$\forall$$x$, ${\it tg}$:Id, $k$:Knd, $l$:IdLnk, $T$, $A$, $B$:Type, $f$:($A$$\rightarrow$$B$$\rightarrow$($T$ List)), ${\it es}$:ES.
\\[0ex]sends $k$(v:$B$) on $l$:
\\[0ex]tagged([$<$${\it tg}$, $\lambda$$s$,$v$. $f$($s$($x$),$v$)$>$],State($x$ : $A$),v):if isrcv($k$)
\\[0ex]then ${\it tg}$ : $T$ $\oplus$ tag($k$) : $B$
\\[0ex]else ${\it tg}$ : $T$
\\[0ex]fi 
\\[0ex]$\Rightarrow$ sends1{-}p(${\it es}$;$x$;$A$;$k$;$B$;$l$;${\it tg}$;$T$;$f$)